Library ConwayNotations
Require Export Reals.
Open Scope R_scope.
Definition sec x := 1/(cos x).
Definition csc x := 1/(sin x).
Definition cot x := 1/(tan x).
Parameter arccos : R → R.
Parameter w : R.
Definition A a b c := arccos((a^2-b^2-c^2)/(-2×b×c)).
Definition B a b c := arccos((-a^2+b^2-c^2)/(-2×a×c)).
Definition C a b c := arccos((-a^2-b^2+c^2)/(-2×a×b)).
Definition SA a b c:= 1/2 × (b^2+c^2-a^2).
Definition SB a b c := 1/2 × (c^2+a^2-b^2).
Definition SC a b c := 1/2 × (a^2+b^2-c^2).
Definition DeltaMaj a b c := 1/4*(sqrt ((a+b-c)*(a-b+c)*(-a+b+c)*(a+b+c))).
Definition SW a b c := 1/2 × (a^2+b^2+c^2).
Definition sa a b c := 1/2 × (b+c-a).
Definition sb a b c := 1/2 × (c+a-b).
Definition sc a b c := 1/2 × (a+b-c).
Definition s a b c := 1/2 × (a+b+c).
Definition SS a b c := 2 × (DeltaMaj a b c).
Definition J a b c := sqrt(a^6-a^4×b^2-a^2×b^4+b^6-a^4×c^2+3×a^2×b^2×c^2-b^4×c^2-a^2×c^4-b^2×c^4+c^6)/(a×b×c).
Definition e a b c := sqrt((a^4-a^2×b^2+b^4-a^2×c^2-b^2×c^2+c^4)/(a^2×b^2+a^2×c^2+b^2×c^2)).
Definition RR a b c := a×b×c/sqrt((((a+b+c)*(b+c-a))*(c+a-b))*(a+b-c)).
Definition r a b c := (1/2)*sqrt((b+c-a)*(c+a-b)*(a+b-c)/(a+b+c)).
Definition TauMaj := (sqrt(5)+1)/2.
Open Scope R_scope.
Definition sec x := 1/(cos x).
Definition csc x := 1/(sin x).
Definition cot x := 1/(tan x).
Parameter arccos : R → R.
Parameter w : R.
Definition A a b c := arccos((a^2-b^2-c^2)/(-2×b×c)).
Definition B a b c := arccos((-a^2+b^2-c^2)/(-2×a×c)).
Definition C a b c := arccos((-a^2-b^2+c^2)/(-2×a×b)).
Definition SA a b c:= 1/2 × (b^2+c^2-a^2).
Definition SB a b c := 1/2 × (c^2+a^2-b^2).
Definition SC a b c := 1/2 × (a^2+b^2-c^2).
Definition DeltaMaj a b c := 1/4*(sqrt ((a+b-c)*(a-b+c)*(-a+b+c)*(a+b+c))).
Definition SW a b c := 1/2 × (a^2+b^2+c^2).
Definition sa a b c := 1/2 × (b+c-a).
Definition sb a b c := 1/2 × (c+a-b).
Definition sc a b c := 1/2 × (a+b-c).
Definition s a b c := 1/2 × (a+b+c).
Definition SS a b c := 2 × (DeltaMaj a b c).
Definition J a b c := sqrt(a^6-a^4×b^2-a^2×b^4+b^6-a^4×c^2+3×a^2×b^2×c^2-b^4×c^2-a^2×c^4-b^2×c^4+c^6)/(a×b×c).
Definition e a b c := sqrt((a^4-a^2×b^2+b^4-a^2×c^2-b^2×c^2+c^4)/(a^2×b^2+a^2×c^2+b^2×c^2)).
Definition RR a b c := a×b×c/sqrt((((a+b+c)*(b+c-a))*(c+a-b))*(a+b-c)).
Definition r a b c := (1/2)*sqrt((b+c-a)*(c+a-b)*(a+b-c)/(a+b+c)).
Definition TauMaj := (sqrt(5)+1)/2.